\begin{tabbing}
d{-}partial{-}world($D$;$f$;${\it t'}$;$s$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\langle$($\lambda$$i$,$x$. M($i$).ds($x$))\+
\\[0ex]$,\,$($\lambda$$i$,$a$. M($i$).da(locl($a$)))
\\[0ex]$,\,$($\lambda$$l$,${\it tg}$. M(source($l$)).dout($l$,${\it tg}$))
\\[0ex]$,\,$($\lambda$$i$,$t$. if $t$$<_{2}$${\it t'}$$\rightarrow$ 1of($f$($t$,$i$)) else $s$($i$) fi)
\\[0ex]$,\,$($\lambda$$i$,$t$. if $t$$<_{2}$${\it t'}$$\rightarrow$ 1of(2of($f$($t$,$i$))) else null fi)
\\[0ex]$,\,$($\lambda$$i$,$t$. if $t$$<_{2}$${\it t'}$$\rightarrow$ 2of(2of($f$($t$,$i$))) else nil fi)
\\[0ex]$,\,$($\lambda$$i$.NullMachine)
\\[0ex]$,\,$$\cdot$$\rangle$
\-
\end{tabbing}